0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 86 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 115 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 0 ms)
↳23 QDP
↳24 Rewriting (⇔, 12 ms)
↳25 QDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 QDP
↳28 QReductionProof (⇔, 0 ms)
↳29 QDP
↳30 Rewriting (⇔, 0 ms)
↳31 QDP
↳32 UsableRulesProof (⇔, 0 ms)
↳33 QDP
↳34 QReductionProof (⇔, 0 ms)
↳35 QDP
↳36 Instantiation (⇔, 0 ms)
↳37 QDP
↳38 QDPOrderProof (⇔, 111 ms)
↳39 QDP
↳40 DependencyGraphProof (⇔, 0 ms)
↳41 TRUE
PERMA_IN_GA(cons(X1, X2), cons(X1, X3)) → U3_GA(X1, X2, X3, appendcB_in_ga(X2, X4))
U3_GA(X1, X2, X3, appendcB_out_ga(X2, X4)) → U4_GA(X1, X2, X3, permA_in_ga(X4, X3))
U3_GA(X1, X2, X3, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U5_GA(X1, X2, X3, X4, splitC_in_gaaa(X2, X5, X3, X6))
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → SPLITC_IN_GAAA(X2, X5, X3, X6)
SPLITC_IN_GAAA(cons(X1, X2), cons(X1, X3), X4, X5) → U1_GAAA(X1, X2, X3, X4, X5, splitC_in_gaaa(X2, X3, X4, X5))
SPLITC_IN_GAAA(cons(X1, X2), cons(X1, X3), X4, X5) → SPLITC_IN_GAAA(X2, X3, X4, X5)
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U6_GA(X1, X2, X3, X4, splitcC_in_gaaa(X2, X5, X3, X6))
U6_GA(X1, X2, X3, X4, splitcC_out_gaaa(X2, X5, X3, X6)) → U7_GA(X1, X2, X3, X4, appendE_in_gga(X5, X6, X7))
U6_GA(X1, X2, X3, X4, splitcC_out_gaaa(X2, X5, X3, X6)) → APPENDE_IN_GGA(X5, X6, X7)
APPENDE_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → U2_GGA(X1, X2, X3, X4, appendE_in_gga(X2, X3, X4))
APPENDE_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPENDE_IN_GGA(X2, X3, X4)
U6_GA(X1, X2, X3, X4, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, X3, X4, appendcD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, appendcD_out_ggga(X1, X5, X6, X7)) → U9_GA(X1, X2, X3, X4, permA_in_ga(X7, X4))
U8_GA(X1, X2, X3, X4, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
appendcB_in_ga(X1, X1) → appendcB_out_ga(X1, X1)
splitcC_in_gaaa(cons(X1, X2), nil, X1, X2) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2), cons(X1, X3), X4, X5) → U16_gaaa(X1, X2, X3, X4, X5, splitcC_in_gaaa(X2, X3, X4, X5))
U16_gaaa(X1, X2, X3, X4, X5, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
appendcD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
appendcE_in_gga(nil, X1, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
PERMA_IN_GA(cons(X1, X2), cons(X1, X3)) → U3_GA(X1, X2, X3, appendcB_in_ga(X2, X4))
U3_GA(X1, X2, X3, appendcB_out_ga(X2, X4)) → U4_GA(X1, X2, X3, permA_in_ga(X4, X3))
U3_GA(X1, X2, X3, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U5_GA(X1, X2, X3, X4, splitC_in_gaaa(X2, X5, X3, X6))
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → SPLITC_IN_GAAA(X2, X5, X3, X6)
SPLITC_IN_GAAA(cons(X1, X2), cons(X1, X3), X4, X5) → U1_GAAA(X1, X2, X3, X4, X5, splitC_in_gaaa(X2, X3, X4, X5))
SPLITC_IN_GAAA(cons(X1, X2), cons(X1, X3), X4, X5) → SPLITC_IN_GAAA(X2, X3, X4, X5)
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U6_GA(X1, X2, X3, X4, splitcC_in_gaaa(X2, X5, X3, X6))
U6_GA(X1, X2, X3, X4, splitcC_out_gaaa(X2, X5, X3, X6)) → U7_GA(X1, X2, X3, X4, appendE_in_gga(X5, X6, X7))
U6_GA(X1, X2, X3, X4, splitcC_out_gaaa(X2, X5, X3, X6)) → APPENDE_IN_GGA(X5, X6, X7)
APPENDE_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → U2_GGA(X1, X2, X3, X4, appendE_in_gga(X2, X3, X4))
APPENDE_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPENDE_IN_GGA(X2, X3, X4)
U6_GA(X1, X2, X3, X4, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, X3, X4, appendcD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, appendcD_out_ggga(X1, X5, X6, X7)) → U9_GA(X1, X2, X3, X4, permA_in_ga(X7, X4))
U8_GA(X1, X2, X3, X4, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
appendcB_in_ga(X1, X1) → appendcB_out_ga(X1, X1)
splitcC_in_gaaa(cons(X1, X2), nil, X1, X2) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2), cons(X1, X3), X4, X5) → U16_gaaa(X1, X2, X3, X4, X5, splitcC_in_gaaa(X2, X3, X4, X5))
U16_gaaa(X1, X2, X3, X4, X5, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
appendcD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
appendcE_in_gga(nil, X1, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
APPENDE_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPENDE_IN_GGA(X2, X3, X4)
appendcB_in_ga(X1, X1) → appendcB_out_ga(X1, X1)
splitcC_in_gaaa(cons(X1, X2), nil, X1, X2) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2), cons(X1, X3), X4, X5) → U16_gaaa(X1, X2, X3, X4, X5, splitcC_in_gaaa(X2, X3, X4, X5))
U16_gaaa(X1, X2, X3, X4, X5, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
appendcD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
appendcE_in_gga(nil, X1, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
APPENDE_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPENDE_IN_GGA(X2, X3, X4)
APPENDE_IN_GGA(cons(X1, X2), X3) → APPENDE_IN_GGA(X2, X3)
From the DPs we obtained the following set of size-change graphs:
SPLITC_IN_GAAA(cons(X1, X2), cons(X1, X3), X4, X5) → SPLITC_IN_GAAA(X2, X3, X4, X5)
appendcB_in_ga(X1, X1) → appendcB_out_ga(X1, X1)
splitcC_in_gaaa(cons(X1, X2), nil, X1, X2) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2), cons(X1, X3), X4, X5) → U16_gaaa(X1, X2, X3, X4, X5, splitcC_in_gaaa(X2, X3, X4, X5))
U16_gaaa(X1, X2, X3, X4, X5, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
appendcD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
appendcE_in_gga(nil, X1, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
SPLITC_IN_GAAA(cons(X1, X2), cons(X1, X3), X4, X5) → SPLITC_IN_GAAA(X2, X3, X4, X5)
SPLITC_IN_GAAA(cons(X1, X2)) → SPLITC_IN_GAAA(X2)
From the DPs we obtained the following set of size-change graphs:
U3_GA(X1, X2, X3, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(cons(X1, X2), cons(X1, X3)) → U3_GA(X1, X2, X3, appendcB_in_ga(X2, X4))
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U6_GA(X1, X2, X3, X4, splitcC_in_gaaa(X2, X5, X3, X6))
U6_GA(X1, X2, X3, X4, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, X3, X4, appendcD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
appendcB_in_ga(X1, X1) → appendcB_out_ga(X1, X1)
splitcC_in_gaaa(cons(X1, X2), nil, X1, X2) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2), cons(X1, X3), X4, X5) → U16_gaaa(X1, X2, X3, X4, X5, splitcC_in_gaaa(X2, X3, X4, X5))
U16_gaaa(X1, X2, X3, X4, X5, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
appendcD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
appendcE_in_gga(nil, X1, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, appendcE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U3_GA(X1, X2, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_in_ga(X2))
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, appendcD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
appendcB_in_ga(X1) → appendcB_out_ga(X1, X1)
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
appendcD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, appendcE_in_gga(X2, X3))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
appendcB_in_ga(x0)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcD_in_ggga(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
U3_GA(X1, X2, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, appendcD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
appendcB_in_ga(X1) → appendcB_out_ga(X1, X1)
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
appendcD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, appendcE_in_gga(X2, X3))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
appendcB_in_ga(x0)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcD_in_ggga(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(X1, X2, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, appendcD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
appendcD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, appendcE_in_gga(X2, X3))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
appendcB_in_ga(x0)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcD_in_ggga(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
appendcB_in_ga(x0)
U3_GA(X1, X2, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, appendcD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
appendcD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, appendcE_in_gga(X2, X3))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcD_in_ggga(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, appendcE_in_gga(X5, X6)))
U3_GA(X1, X2, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, appendcE_in_gga(X5, X6)))
appendcD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, appendcE_in_gga(X2, X3))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcD_in_ggga(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(X1, X2, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, appendcE_in_gga(X5, X6)))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcD_in_ggga(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
appendcD_in_ggga(x0, x1, x2)
U3_GA(X1, X2, appendcB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, appendcE_in_gga(X5, X6)))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(z0, z1, appendcB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, appendcE_in_gga(X5, X6)))
U3_GA(z0, z1, appendcB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U6_GA(X1, X2, splitcC_out_gaaa(X2, X5, X3, X6)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, appendcE_in_gga(X5, X6)))
U3_GA(z0, z1, appendcB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
POL(PERMA_IN_GA(x1)) = x1
POL(U16_gaaa(x1, x2, x3)) = 1 + x3
POL(U17_gga(x1, x2, x3, x4)) = 1 + x4
POL(U18_ggga(x1, x2, x3, x4)) = x4
POL(U3_GA(x1, x2, x3)) = 1 + x2
POL(U6_GA(x1, x2, x3)) = 1 + x3
POL(U8_GA(x1, x2, x3)) = x3
POL(appendcB_out_ga(x1, x2)) = 0
POL(appendcD_out_ggga(x1, x2, x3, x4)) = x4
POL(appendcE_in_gga(x1, x2)) = 1 + x1 + x2
POL(appendcE_out_gga(x1, x2, x3)) = 1 + x3
POL(cons(x1, x2)) = 1 + x2
POL(nil) = 0
POL(splitcC_in_gaaa(x1)) = x1
POL(splitcC_out_gaaa(x1, x2, x3, x4)) = 1 + x2 + x4
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, splitcC_in_gaaa(X2))
U8_GA(X1, X2, appendcD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, appendcB_out_ga(X2, X2))
appendcE_in_gga(nil, X1) → appendcE_out_gga(nil, X1, X1)
appendcE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, appendcE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, appendcE_out_gga(X2, X3, X4)) → appendcE_out_gga(cons(X1, X2), X3, cons(X1, X4))
splitcC_in_gaaa(cons(X1, X2)) → splitcC_out_gaaa(cons(X1, X2), nil, X1, X2)
splitcC_in_gaaa(cons(X1, X2)) → U16_gaaa(X1, X2, splitcC_in_gaaa(X2))
U16_gaaa(X1, X2, splitcC_out_gaaa(X2, X3, X4, X5)) → splitcC_out_gaaa(cons(X1, X2), cons(X1, X3), X4, X5)
splitcC_in_gaaa(x0)
U16_gaaa(x0, x1, x2)
appendcE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)